mcsta

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:actuators (prob-reach)
Invocation (default)
mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props actuators -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --p0 --p1
Execution
Walltime:7.284163236618042s
Return code:0
Note(s):The tool result '646935642857007/6250000000000000' is tagged as incorrect. The reference result is '2486339329126654286603009697501669410565922080647235572297420531003436740865701642894224651957236979415804844019970070797212838741320749871087696043790430488516768144231337033817746564261751745074561347394006816495027017797689319547300488225074500148562849173672852142305219348461967484204844049064729196699735928014471258755257981315981437194941990940151801223037104684834501918219518509576147895594521550143080313306069328271572867233516691965651482621705351476665971739605138196440899155147689763504549588268208121401875264463514032072760483012146809591389917819090345027584564812047944749664670576370371539376963526238191240909958985452275278006429583432435031807238331342878089585624527146895090748546393263058273883548791148930403418281798548198424839109773636808627978181634014955673865189747661646872651996258392552936446048778850218123619968642035042613279480618036150872134108049644406926052409061681799637826350380022669199996003596956454782552145333056157894145489486150540020412367389756815095367155100979032989577219964876141639524244527608740339422128257119204903748534580255367130745069830155822896692205418889181867570399342666796568670310583910515081237965368477709014032538181219194690388788147910806457016503932544044361342482618424045300689342156932654513810653232/23611139712102051230917389163705830960031855919193061353466918264830083378326191986369644719731733927229539492600419384037259194731474764121283541927110582338954972260482489069672524784993784262550354865456872177586787640220120819688039079785300002792915291730955593483931646644219725546280035297145057925920216590907280123192615618204899469159482885775117640880607396241557854775904114044868093404127365731780383766098536743365431606149805147123738769862714193052746662633506746823832901275751745965930188386773348462353851130634494111719846304545619011283033383773694078253680336971342463788449790335853827682934039541430969389834393278233712786556823508225268957600063594542555015850051657407051988438160129534133247921531327619001040045086238243881240503946765414870850573700427770606192511529412103367398696559809991483002140786128316014280845971470100880405232693440182197432483126227685144563355464988202359315240457890538240804613319209327258473954661426136227180487183808347011148390279684571713981594509718194717843432940624635810976882203361528885015337153218704100617865345448218447207127579308191723103792137390005496384380796220104269395092237919302086773300230575431863081466614429004067089423894856968938002028941688162575178715549796054402371237245066557533118053584375' (approx. 0.1053036557931282) which means a relative error of '0.01703599863172215' which is larger than the goal precision '0.001'.
Relative Error:0.01703599863172215
Log
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.

Peak memory usage: 53 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0

+ State space exploration
  State size:  16 bytes
  States:      5820
  Transitions: 5820
  Branches:    16788
  Rate:        85588 states/s
  Time:        0.1 s

+ Property actuators
  Probability: 0.10350970285712112
  Bounds:      [0.10350970285712112, 1]
  Time:        6.7 s

  + Precomputations
    Min. prob. 0 states:          4512
    Time for min. prob. 0 states: 0.0 s
    Min. prob. 1 states:          180
    Time for min. prob. 1 states: 0.0 s

  + Essential states
    Iterations:       1
    Essential states: 1130
    Transitions:      1130
    Branches:         7386
    Time:             0.0 s

  + Value iteration
    Final error: 9.999901531850148E-07
    Iterations:  94800
    Time:        6.7 s

Exported results to file "/out.txt".	
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.